00100	(GIVEAX EVSUM
00200	 ((FORALL X)
00300	  ((FORALL Y)
00400	   (IMPLIES (AND (MEMBER X I) (MEMBER Y I))
00500		    (EQUAL (PLUS X Y) (EVAL (LIST (QUOTE PLUS) X Y)))))))
00600	
00700	
00800	(PROOF ONE) 
00900	1 	(USEAX EVSUM (QUOTE 17) (QUOTE 34))
01000	2 	(INTQUOTE 17)
01100	3 	(INTQUOTE 34)
01200	4 	(ISINT 17)
01300	5 	(ISINT 34)
01400	6 	(REPL 4 2 1)
01500	7 	(REPL 5 3 1)
01600	8 	(AI 6 7)
01700	9 	(MP 8 1)
01800	10 	(EVLIST (QUOTE PLUS) (QUOTE 17) (QUOTE 34))
01900	11 	(REPL 9 10 1)
02000	12 	(EVEVAL (PLUS 17 34))
02100	13 	(REPL 11 12 1)
02200	14 	(REPR 13 3 1)
02300	15 	(REPR 14 2 1)
02400	16 	(INTQUOTE 51)
02500	17 	(REPR 15 16 1)